\documentclass{beamer}
\usetheme{Madrid} % My favorite!
%\usetheme{Boadilla} % Pretty neat, soft color.
%\usetheme{default}
%\usetheme{Warsaw}
%\usetheme{Bergen} % This template has nagivation on the left
%\usetheme{Frankfurt} % Similar to the default 
%with an extra region at the top.
%\usecolortheme{beaver} % Simple and clean template
%\usetheme{Darmstadt} % not so good
% Uncomment the following line if you want %
% page numbers and using Warsaw theme%
% \setbeamertemplate{footline}[page number]
%\setbeamercovered{transparent}
\usepackage{ucs}
\usepackage[utf8x]{inputenc} % Включаем поддержку UTF8
\usepackage[russian]{babel} 

\setbeamercovered{invisible}
% To remove the navigation symbols from 
% the bottom of slides%
\setbeamertemplate{navigation symbols}{} 
%
\usepackage{graphicx}
\newcounter{N}
%\usepackage{bm}         % For typesetting bold math (not \mathbold)
%\logo{\includegraphics[height=0.6cm]{yourlogo.eps}}
%
\title[Исследование систем типизированного $\lambda$-исчисления]{Реализация и исследование систем типизированного $\lambda$-исчисления 
с контролем изменений наиболее общего типа}
\author[Кристина Курьян]{Кристина Курьян\\{\small Руководитель: Москвин Д. Н.}}
\institute{Санкт-Петербургский Академический университет}
\date{\today}
% \today will show current date. 
% Alternatively, you can specify a date.
%
\begin{document}
%
\begin{frame}
\titlepage
\end{frame}
%

\section{Теория}

\begin{frame}[fragile]
  \frametitle{Теория (1)}   % Insert frame title between curly braces
  В $\lambda$ -исчислении две операции: применение и абстракция.
  \begin{description}
  \item[Применение (Application):] \hspace*{\fill} \\
  F X \\  
  С точки зрения программиста: \\
  F (алгоритм) применяется к X (входные данные).  \\
   \\
  \item[Абстракция (Abstraction):] \hspace*{\fill} \\
  Пусть M = M[x] — выражение, содержащее x. \\
  Тогда $\lambda$ x. M обозначает функцию x $\to$ M[x], \\
  то есть каждому x сопоставляется M[x].\\			
  \end{description}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}


\begin{frame}[fragile]
  \frametitle{Теория (2)}   % Insert frame title between curly braces

  \begin{itemize*}
   Применение и абстракция работают совместно: \\
   ($\lambda$x. x + 3) 39 = 42 \\
   \hspace*{\fill} \\
   Def. Отношение $\beta$-редукции $\to_{\beta}$ над $\Lambda$ :\\
   ($\lambda$x.M) N $\to_{\beta}$  M[x := N] \\
   Пример:\\
   ($\lambda$yz.y)($\lambda$p.p) $\to_{\beta}$ $\lambda$zp.p \\ 
   \hspace*{\fill} \\
   Def. Экспансия - операция обратная редукции\\ 
  \end{itemize*}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}

\begin{frame}[fragile]
  \frametitle{Теория (3)}   % Insert frame title between curly braces

  \begin{itemize*}
   & {\color{blue}Типизация термов} \\
   & Если терм переменная — как угодно :\\
   & x: $\alpha$, y: $\alpha$ \to $\beta$\\
   & Если терм аппликация MN, то \\
   & 1. M должно быть функцией, то есть иметь стрелочный тип \\
   & M: $\sigma$ \to $\tau$\\
   & 2. N должно быть «подходящим» аргументом, то есть иметь \\
   & тип N:$\sigma$\\
   & 3. вся аппликация должна иметь тип результата применения \\
   & функции: (MN):$\tau$\\
   & Пример: x: $\alpha$, y: $\alpha$ \to $\beta$. Тогда (xy):$\beta$\\
  \end{itemize*}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}


\begin{frame}[fragile]
  \frametitle{Теория (4)}   % Insert frame title between curly braces

  \begin{itemize*}
   & Если терм абстракция $\lambda$x.M, то тип должен быть стрелоч- \\
   & ным ($\lambda$x.M) : $\sigma$ \to $\tau$, причём тип аргумента x : $\sigma$ и тип тела \\ 
   & абстракции M:$\tau$\\
   & Пример:x: $\alpha$ имеем ($\lambda$x. x) : $\alpha$ \to $\alpha$.\\
   &  \hspace*{\fill} \\
   & Рассмотрим последовательностей редукций \\ 
   & M $\to_{\beta}$ M` $\to_{\beta}$ M``\\ 
   & Припишем каждому редексу тип: \\ 
   & M: $\tau$ $\to_{\beta}$ M`: $\tau$ $\to_{\beta}$ M``: $\tau$ \\ 
  \end{itemize*}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}

\begin{frame}[fragile]
  \frametitle{Теория (5)}   % Insert frame title between curly braces

  \begin{itemize*}
   & Вопрос: когда сохраняется тип при экспансии и когда нет? \\ 
   & Рассмотрим как пример нумералы Черча \\ 
   & Def. Нумералы Черча\\
   & 0 = $\lambda$s z. z \\
   & 1 = $\lambda$ s z. s z \\
   & 2 = $\lambda$ s z. s (s z) \\
   & 3 = $\lambda$ s z. s (s (s z)) \\
   & 4 = $\lambda$ s z. s (s (s (s z)))\\
   & ... \\
  \end{itemize*}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}

\begin{frame}[fragile]
  \frametitle{Теория (6)}   % Insert frame title between curly braces

  \begin{itemize*}
   & Припишем типы к нумералам Черча:\\
   & 0: \alpha \to \beta \to \beta \\
   & 1: (\beta \to \gamma) \to \beta \to \gamma \\
   & 2: (\beta \to \beta) \to \beta \to \beta \\
   & .. \\
   & n: (\beta \to \beta) \to \beta \to \beta \\
   & Запишем разность между 2 нумералами, к примеру: \\	
   & 5 - 4 = 1, 3 - 3 = 0\\	
   & \\	
   & С одной стороны ясно что тип результата должен быть\\	
   & (\beta \to \beta) \to \beta \to \beta \\	
   & Но с другой стороны: \\
   & \alpha \to \beta \to \beta \\ 
  \end{itemize*}
\end{frame}
\note[enumerate]       % Add notes to yourself that will be displayed when
{                      % typeset with the notes or notesonly class options
\item Note for Point 1   
\item Note for Point 2   
}


\section{Постановка задачи}

\begin{frame} 
  \frametitle{Постановка задачи}	
  {\color{blue}Постановка задачи: } \\	
  Исследовать эффект изменения типа при экспансии \\
  \hspace*{\fill} \\
  {\color{blue}Шаги:} \\	
  \begin{itemize}
    \item Реализовать систему редукции.
    \item Реализовать систему вывода типов.
    \item Определить условия, при которых имеет место эффект изменения типа.
  \end{itemize}
\end{frame} 

\section{Результаты}

\begin{frame} 
  \frametitle{Результаты (1)}	
  Для системы просто типизированного $\lambda$ исчисление реализованы
  \begin{itemize}
    \item Система пошаговой редукции термов.
    \item Система вывода типов на основе построения системы уравнений на типы и их решения.
  \end{itemize}
  Помимо этого:
  \begin{itemize}
    \item Алгоритмы расширены для работы со свободными переменными. 
    \item Реализована проверка что тело и типа лямбда выражения является функцией типа из типов аргументов и типа тела. \\
    \item Реализована подсистема строкового ввода-вывода термов и их типов.
  \end{itemize}
\end{frame} 


\begin{frame} 
  \frametitle{Результаты (2)}	
  Реализована подсистема System Fw $\in$ System F \\
  Для ней были реализованы \\
  \begin{itemize}
    \item AllowType
    \item CheckType 
  \end{itemize}
  Помимо этого:
  \begin{itemize}
    \item Она были расширена для работы с подсистемой ML. 
    \item Подтверждены теоретические результаты для ML.
  \end{itemize}

\end{frame} 

\section{Выводы}

\begin{frame}[fragile]
  \frametitle{Выводы}   % Insert frame title between curly braces
  Эффект изменения наиболее общего типа появляется в системах:
  \begin{description}
  \item[Просто типизированное $\lambda$ -исчисление] \hspace*{\fill} \\
  Когда при редукции одно из уравнений на типы исчезает \\
  \item[System Fw] \hspace*{\fill} \\
  Для системы ML - эффект появляется при редукции одно из уравнений исчезает \\			
  \end{description}
\end{frame}

% End of slides
\end{document}
